Nuprl Lemma : d-single-sframe_wf
11,40
postcript
pdf
i
:Id,
L
:(Knd List),
l
:IdLnk,
tg
:Id. @
i
: only
L
sends on (
l
with
tg
)
Dsys
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
Dsys
,
@
i
: only
L
sends on (
l
with
tg
)
Lemmas
ifthenelse
wf
,
eqof
wf
,
Id
wf
,
id-deq
wf
,
msga
wf
,
ma-single-sframe
wf
,
ma-empty
wf
,
IdLnk
wf
,
Knd
wf
origin
i:Id, L:(Knd List), l:IdLnk, tg:Id. @i: only L sends on (l with tg) 
Dsys i:Id, L:(Knd List), l:IdLnk, tg:Id. @i: only L sends on (l with tg) Dsys x:A. B(x) T